$\forall$$A$:Type, $B$, $C$:($A$$\rightarrow$Type), $f$:$a$:$A$ fp$\rightarrow$ $B$($a$), $g$:($\cap$$a$:$A$.$B$($a$)$\rightarrow$$C$($a$)). $g$ o $f$ $\in$ $a$:$A$ fp$\rightarrow$ $C$($a$)